Is it formalized somewhere that metric-space-of-short-functions-Metric-Space A is right adjoint to "product-Metric-Space A", so that this can confidently be used for "binary short functions"?

Otherwise that might be a good sanity-check to formalize

Is it formalized somewhere that metric-space-of-short-functions-Metric-Space A is right adjoint to "product-Metric-Space A", so that this can confidently be used for "binary short functions"?

I don't think so, we didn't do much in the categorical POV of metric spaces. I don't think we even have the concept "product-Metric-Space A" Do you think it's true? If so, I guess we could add this result sometimes in the future. I've never worked with right adjoints and I'm still working on #1421 so I'll need some time to think about it.

It might be true, and I think it is a question worth considering since you are defining what it means to be a binary short function here. If it is not true you may be giving a wrong definition. The adjointedness condition I mention is known in the literature as cartesian closedness, and means that we can observe collections of morphisms in the category as internal objects in the category itself. E.g., given that it is true, the metric space of short functions between two metric spaces represent in a concrete sense the collection of short functions viewed internally. The concrete way in which it represents this collection is precisely by the equivalence

$$\mathrm{Hom}(A \times B, C) \cong \mathrm{Hom}(A, C^B)$$

Where $\mathrm{Hom}$ is the type of short functions, $A \times B$ is the product metric space, and $C^B$ is the metric space of short functions. This equivalence is what the adjointedness condition I mention would unfold to.

The question I'd like you to ask yourself is: what is the difference between

    short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A)

and

    short-function-Metric-Space (product-Metric-Space A A) A

Are they the same? If so, there is no problem.

So, basically, I could construct an isometry

  isometry-ev-pair-short-function-product-Metric-Space :
    isometry-Metric-Space
      ( metric-space-of-short-functions-Metric-Space
        ( product-Metric-Space X Y)
        ( Z))
      ( metric-space-of-short-functions-Metric-Space
        ( X)
        ( metric-space-of-short-functions-Metric-Space Y Z))

and and inverse in the space of functions product-Metric-Space X Y -> Z

  map-ind-short-function-product-Metric-Space :
    short-function-Metric-Space
      ( X)
      ( metric-space-of-short-functions-Metric-Space Y Z) →
    map-type-Metric-Space
      ( product-Metric-Space X Y)
      ( Z)

If the latter takes value in the space of short functions, then we have

    metric-space-of-short-functions-Metric-Space
      ( product-Metric-Space X Y)
      ( Z) ＝
    metric-space-of-short-functions-Metric-Space
      ( X)
      ( metric-space-of-short-functions-Metric-Space Y Z)

but I don't know how to prove this last step. Do you have any idea how to complete this proof? Or maybe it's not always true?

If anyone is reading this:

• with this setting, I can prove that map-ind-short-function-product-Metric-Space f is uniformly continuous, but still not short;
• I'm starting to believe it's not true: add-ℚ is a

short-function-Metric-Space
  ( ℚ)
  ( metric-space-of-short-functions-Metric-Space ℚ ℚ)

but I don't think it's short as a function product-Metric-Space ℚ ℚ → ℚ.

So, regarding #1447 (comment), let's assume they're not the same and we have a problem. How should we solve it?

NB: whatever the definition of Metric-Semigroup ends up being, I think we'd want ℚ , add-ℚ to be an instance of it.

It seems impossible to me that add-ℚ is not a short function viewed as product-Metric-Space ℚ ℚ → ℚ, considering it is commutative. Are you sure this is the case?

Based on this Wikipedia page, I propose you define the product metric space using the supremum, i.e. maximum distance of the coordinates, and then use short-function-Metric-Space (product-Metric-Space A A) A in your definitions. This should always be correct, and then we can later resolve the question of wheter short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A) is equivalent or not.

Based on this Wikipedia page, I propose you define the product metric space using the supremum, i.e. maximum distance of the coordinates,

I think that's what this definition does: upper bounds of the "product distance" are upper bounds on each coordinates, i.e. upper bounds of the max if the distances. This is also coherent with the definition of "dependent product of metric spaces" where the distance is the supremum.

It seems impossible to me that add-ℚ is not a short function viewed as product-Metric-Space ℚ ℚ → ℚ, considering it is commutative.

I was surprised too, and I don't see how commutativity should help...

Are you sure this is the case?

Unless I'm mistaken, it basically boils down to proving that

|(x + y) - (x' + y')| ≤ max (|x - x'| , |y - y'|) 

and I don't see a way out. It is a lipschitz-function-Metric-Space (product-Metric-Space A A) A though. Would that help?

then use short-function-Metric-Space (product-Metric-Space A A) A in your definitions. This should always be correct, and then we can later resolve the question of wheter short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A) is equivalent or not.

So ℚ , add-ℚ will not be a metric semigroup?

and in fact there is an infinite family of equivalent choices of metric on the product. One for every "real number" in $(0,\infty]$. The canonical choice is $\infty$.

which is what you've chosen below I think

looks like you could add is-tight-structure-product-Metric-Space as another lemma?

why not call it premetric-product-Metric-Space?

after #1421 there will be no more "premetrics". With #1450 this would probably be something like

neighborhood-prop-product-Metric-Space : Rational-Neighborhood-Relation (l2 ⊔ l4) type-product-Metric-Space

Wait, doesn't this show that the category of metric spaces is cartesian closed? 🤩

Oh, I see, isometries don't characterize equality

That's a bummer. So then only the category of "metric spaces up to isometry" is cartesian closed

Still I find it strange if they are not equivalent...